Леонова М. А. , Девянин П. Н. «Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB» // Прикладная дискретная математика 2021. №52 C.83-96